s:QOSet, a, b, c:|s|. (a  b)  (b <s c)  (a <s c) 

latex

Up	sets 1
Definitions of Statement	DSet, QOSet
Definitions	P & Q, x,y. t(x;y), x. t(x), t  T, , P  Q, P  Q, P  Q, x:A. B(x), {T}, x(s1,s2), DSet, x(s), QOSet
Lemmas	set lt is sp of leq, implies functionality wrt iff, strict part wf, set lt wf, set leq wf, set car wf, qoset wf, all functionality wrt iff, set leq trans, trans imp sp trans a